/* @LICENSE(NICTA_CORE) */

#ifndef __LIBSEL4_TYPES_H
#define __LIBSEL4_TYPES_H

#include <sel4/macros.h>
#include <sel4/arch/types.h>

typedef enum {
    seL4_SysSend            = -1,
    seL4_SysNBSend          = -2,
    seL4_SysCall            = -3,
    seL4_SysWait            = -4,
    seL4_SysReply           = -5,
    seL4_SysReplyWait       = -6,
    seL4_SysPoll            = -7,
    seL4_SysYield           = -8,
    seL4_SysDebugPutChar    = -9,
    seL4_SysDebugHalt       = -10,
    seL4_SysDebugSnapshot   = -11,
    seL4_SysDebugRun        = -12,
    SEL4_FORCE_LONG_ENUM(seL4_Syscall_ID),
} seL4_Syscall_ID;

typedef enum {
    seL4_UntypedObject = 0,
    seL4_TCBObject,
    seL4_EndpointObject,
    seL4_AsyncEndpointObject,
    seL4_CapTableObject,
    seL4_NonArchObjectTypeCount,
    SEL4_FORCE_LONG_ENUM(seL4_ObjectType),
} seL4_ObjectType;

typedef enum {
    seL4_NoError = 0,
    seL4_InvalidArgument,
    seL4_InvalidCapability,
    seL4_IllegalOperation,
    seL4_RangeError,
    seL4_AlignmentError,
    seL4_FailedLookup,
    seL4_TruncatedMessage,
    seL4_DeleteFirst,
    seL4_RevokeFirst,
    seL4_NotEnoughMemory,
    SEL4_FORCE_LONG_ENUM(seL4_Error),
} seL4_Error;

typedef enum {
    seL4_NoFault = 0,
    seL4_CapFault,
    seL4_VMFault,
    seL4_UnknownSyscall,
    seL4_UserException,
    seL4_Interrupt,
    SEL4_FORCE_LONG_ENUM(seL4_FaultType),
} seL4_FaultType;

typedef enum {
    seL4_NoFailure = 0,
    seL4_InvalidRoot,
    seL4_MissingCapability,
    seL4_DepthMismatch,
    seL4_GuardMismatch,
    SEL4_FORCE_LONG_ENUM(seL4_LookupFailureType),
} seL4_LookupFailureType;

typedef enum {
    seL4_CanWrite = 0x01,
    seL4_CanRead = 0x02,
    seL4_CanGrant = 0x04,
    seL4_AllRights = seL4_CanWrite|seL4_CanRead|seL4_CanGrant,
    seL4_Transfer_Mint = 0x100,
    SEL4_FORCE_LONG_ENUM(seL4_CapRights),
} seL4_CapRights;

#define seL4_GuardSizeBits 5
#define seL4_GuardBits 18

#define seL4_BadgeBits 28

typedef union {
    seL4_Word raw;
    struct {
#ifdef BIG_ENDIAN
        seL4_Word _padding1 : seL4_WordBits - seL4_GuardBits - seL4_GuardSizeBits - 3;
        seL4_Word guard_bits : seL4_GuardBits;
        seL4_Word guard_size : seL4_GuardSizeBits;
        seL4_Word _padding : 3;
#else
        seL4_Word _padding : 3;
        seL4_Word guard_size : seL4_GuardSizeBits;
        seL4_Word guard_bits : seL4_GuardBits;
#endif
    } _guard;
#ifdef BIG_ENDIAN
    struct {
        seL4_Word _padding : seL4_WordBits - seL4_BadgeBits;
        seL4_Word badge : seL4_BadgeBits;
    } _badge;
#else
    struct {
        seL4_Word badge : seL4_BadgeBits;
        seL4_Word _padding : seL4_WordBits - seL4_BadgeBits;
    } _badge;
#endif
} seL4_CapData;

// Wrapper macros currently use deprecated bitfields.
// TODO: Use bitfield generator?
#define seL4_CapData_MakeGuard(x,y) ((seL4_CapData){._guard = {.guard_bits = (y),.guard_size=(x)}})
#define seL4_CapData_MakeBadge(x) ((seL4_CapData){._badge = {.badge = (x)}})
#define seL4_CapData_GetBadge(x) ((x)._badge.badge)
#define seL4_CapData_GetGuardSize(x) ((x)._guard.guard_size)
#define seL4_CapData_GetGuardBits(x) ((x)._guard.guard_bits)

#define seL4_NilData (seL4_CapData)(seL4_Word)0

#define seL4_MsgLengthBits 7
#define seL4_MsgMaxLength 120
#define seL4_MsgExtraCapBits 2
#define seL4_MsgMaxExtraCaps ((1<<seL4_MsgExtraCapBits)-1)
#define seL4_LabelBits (seL4_WordBits-seL4_MsgLengthBits-seL4_MsgExtraCapBits-seL4_MsgMaxExtraCaps)
#define seL4_UntypedRetypeMaxObjects 256

typedef union {
    struct {
#ifdef BIG_ENDIAN
        seL4_Word label : seL4_LabelBits;
        seL4_Word capsUnwrapped : seL4_MsgMaxExtraCaps;
        seL4_Word extraCaps : seL4_MsgExtraCapBits;
        seL4_Word length : seL4_MsgLengthBits;
#else
        seL4_Word length : seL4_MsgLengthBits;
        seL4_Word extraCaps : seL4_MsgExtraCapBits;
        seL4_Word capsUnwrapped : seL4_MsgMaxExtraCaps;
        seL4_Word label : seL4_LabelBits;
#endif
    };
    seL4_Word raw;
} seL4_MessageInfo;

typedef struct _seL4_IPCBuffer {
    seL4_MessageInfo tag;
    seL4_Word msg[seL4_MsgMaxLength];
    seL4_Word userData;
    union {
        seL4_CPtr caps[seL4_MsgMaxExtraCaps];
        seL4_CapData badges[seL4_MsgMaxExtraCaps];
    };
    seL4_CPtr receiveCNode;
    seL4_CPtr receiveIndex;
    seL4_Word receiveDepth;
} seL4_IPCBuffer __attribute__ ((__aligned__ (sizeof(struct _seL4_IPCBuffer))));

typedef seL4_CPtr seL4_CNode;
typedef seL4_CPtr seL4_IRQHandler;
typedef seL4_CPtr seL4_IRQControl;
typedef seL4_CPtr seL4_TCB;
typedef seL4_CPtr seL4_Untyped;

#include <sel4/arch/constants.h>

#endif
